es:ES, e, e':E. first(e)  loc(e) = loc(e')  Id  e  e'  

latex

Definitions	e  e' , t  T, P  Q, x:A. B(x), ES, E, first(e), b, loc(e), Id, Prop, P  Q, P & Q, P  Q
Lemmas	es-le-not-locl, Id wf, es-loc wf, assert wf, es-first wf, es-E wf, event system wf, es-first-implies